nLab opetopic type theory

Idea

Opetopic type theory (Finster 12) is a higher dimensional directed homotopy type theory for omega-categories, i.e. of infinity-categories in the full sense of $(\infty,\infty)$-categories. Specifically, it realizes the higher-dimensional horn-filler conditions in the definition of opetopic omega-categories due to Palm as inference rules of term introduction for a higher-dimensional kind of formal logic (but it presently ignores the saturation condition on the thin cells).

Where in homotopy type theory there is an identity type of any type axiomatizing the infinity-groupoid structure of that type in, effectively, the style of a globular omega-groupoid, in opetopic type theory there is axiomatized instead a type of k-morphisms for all $k$ in the shape of opetopes.

Hence given a base type $\mathbf{B}\mathcal{U}$ – and a priori there is just one, to be thought of as the categorically delooped type universe, see below – a type is thus effectively identified with the shape of an opetope and thought of as the type of k-morphisms in $\mathbf{B}\mathcal{U}$, the only other data being a possible marking that identifies it as just the sub-type of $k$-equivalences of the given opetopic shape.

The only deduction rule is opetopic type formation and a term introduction rule which expresses the evident Kan filler-like condition saying that if a term of given opetopic shape is an outer horn (here: a “nook”) of $k$-cells, then a $k$-dimensional filler term is deduced, and if an outer or inner horn has a boundary by equivalences then a filler term marked as an equivalence is deduced.

Due to the genuinely omega-categorical nature of the setup, it makes sense to think of the (a priori) unique base type $\mathbf{B}\mathcal{U}$ as the categorical delooping of a type universe $\mathcal{U}^\times$ being a monoidal (infinity,n)-category omega-category, and hence of the 1-endomorphisms (hence the terms of shape the directed interval $(\mathbf{B}\mathcal{U}\to \mathbf{B}\mathcal{U})$ ) as being the types in that universe. Composition of 1-morphism hence implies a type formation for multiplicative conjunction-types in a directed kind of linear homotopy type theory.

Introducing an axiom to this system just means postulating terms of (the type of) the shape of prescribed opetopes. For example:

• $n$-truncation – For the language inside an (infinity,n)-category one demands that all k-morphisms for $k \geq n+1$ are marked as equivalences;

• $k$-adjoints – To axiomatize that two $k$-morphism are left adjoint and right adjoint to each other, respectively, one postulates the existence of $k+1$-morphisms serving as unit of an adjunction and counit of an adjunction and of a 3-morphism marked as equivalence which axiomatizes the zig-zag identities.

Imposing $n$-trunction and adjoints for all k-morphisms for $0 \leq k \leq n$ therefore axiomatizes the language for a free (infinity,n)-category with adjoints on a single object. Categorical looping (which is immediate and primitive in the system, as above) hence gives the free (infinity,n)-category with duals on a single object.

This is the structure to which the cobordism hypothesis applies. Of course the proof of the cobordism hypothesis is not formulated in opetopic type theory and one would have to show that the language it is formulated in is suitably equivalent to that of opetopic type theory, but inspection in low dimension shows that the higher dimensional traces that opetopic type theory produces are of just the right kind.

Related entries

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

  • 1lab (cross-linked reference resource)

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

References

Opetopic type theory is due to

• Eric Finster, Type Theory and the Opetopes, talk at Polish Seminar on Category Theory and its Applications, June 2012 (pdf)

It syntactically implements the definition of opetopic omega-category due to

• Thorsten Palm, …

by interpreting the higher-dimensional horn-filler conditions given there as inference rules.

(Palm shows that any opetopic set satisfying these filler conditions satisfies the property of Michael Makkai‘s definition of a opetopic set that qualifies as an opetopic omega-category. The converse is presently unknown.)

The higher dimensional string diagram-notation used here for opetopes was introduced (as “zoom complexes” in section 1.1) in

• Joachim Kock, André Joyal, Michael Batanin, Jean-François Mascari, Polynomial functors and opetopes (arXiv:0706.1033)

Animated exposition of this higher-dimensional string-diagram notation is in

• Eric Finster, Opetopic Diagrams 1 - Basics (video)

• Eric Finster, Opetopic Diagrams 2 - Geometry (video)

A computer proof assistant for working with opetopic type theory is

• Eric Finster, Orchard (GitHub repository)

• Eric Finster, Opetope! (online opetopic type theory system)

A video tutorial for Orchard is

• Eric Finster, Orchard 1 - Introduction (video)

• Eric Finster, Orchard 2 - Modifying the shape (video)

• Eric Finster, Orchard 3 - Composition and associativity (video)

• Eric Finster, Orchard 4 - Identities and invertibility (video)

Apparently Orchard is discontinued in favour of an online version of similar functionality:

• Eric Finster, Opetopic (GitHub repository) (Website)

Something like an implementation of aspects of opetopic type theory within homotopy type theory is described in

• Eric Finster, Towards Higher Universal Algebra in Type Theory, Homotopy Type Theory Electronic Seminar 2018 (recording, Agda code)

• Antoine Allioux, Eric Finster, Matthieu Sozeau, Types are internal infinity-groupoids, 2021 (hal:03133144, pdf)

• Eric Finster, The $(\infty,1)$-category of Types, talk at CQTS (Dec 2022) [slides: pdf, video: rec]

  Abstract: A major outstanding difficulty in Homotopy Type Theory is the description of coherent higher algebraic structures. As an example, we know that the algebraic structure possessed by the collection of types and functions between them is not a traditional 1-category, but rather an (∞,1)-category. In this talk, I will describe how the addition of a finite collection of additional definitional equalities designed to render the notion of “opetopic type” definable in fact allows one to construct the (∞,1)-category structure on the universe of types.